(set-logic HORN)
(set-option :fp.engine bmc)
(set-option :fp.xform.bit_blast true)
(assert (forall ((q4 (_ BitVec 12)) (q5 (_ BitVec 12)) (q6 (_ BitVec 12)) (q7 (_ BitVec 9))) (= q5 (_ bv0 12))))
(check-sat)
(reset)
(set-logic HORN)
(set-option :fp.engine spacer)
(set-option :fp.xform.bit_blast true)
(assert (forall ((q3 (_ BitVec 1)) (q4 (_ BitVec 1)) (q5 (_ BitVec 10))) (distinct q3 (_ bv0 1))))
(check-sat)
(reset)
(set-option :fp.xform.bit_blast true)
(assert (forall ((a (_ BitVec 10))) (= (bvmul a a) a)))
(check-sat-using horn)